/*
**************************************************************************************************************
File:         ddr3_assertions.sv
Description:  Defines the assertions used in verifying the DDR3 interface
Author     :  Rohit Kulkarni
              Aditya Joshi
**************************************************************************************************************
*/
import params_pkg::*;

module ddr3_assertions(  
  controller  DDR_controller,
  DDR_bus IF
);
  
  //Property to verify RAS signal transitions during activate
  property RASL2RASH;
   @(posedge IF.CK)
     $fell(IF.RAS) |-> ##(tRCD-1) $rose(IF.RAS);
  endproperty
  RASL2RASH_1: assert property(RASL2RASH)  
  else
    $error("Violated tRCD requirement");
        
  //Property to verify CAS signal transitions during Read/Write    
  property CASL2CASH;                           //verify CAS fall and rise time
   @(posedge IF.CK)
  	$fell(IF.CAS) |-> ##tCL $rose(IF.CAS);
  endproperty
  CASL2CASH_1: assert property(CASL2CASH)
  else 
    $error("Violated tCL requirement");

  //Property to verify time between RAS going low in activate and data changing on DQ
  property RASL2DOUT;                           
   @(posedge IF.CK)
  	$fell(IF.RAS) |-> ##(tRCD + tCL) $changed(IF.DQ);
  endproperty
  RASL2DOUT_1: assert property(RASL2DOUT)
  else 
    $error("Violated tRCD + tCL requirement");
    

  //Property to verify read to precharge time    
  property Read2Precharge;                        
   @(posedge IF.CK)
  	($fell(IF.CAS) && $rose(IF.RAS))|-> ## (tCL + tDout) $fell(IF.RAS);
  endproperty
  Read2Precharge_1: assert property(Read2Precharge)
  else 
    $error("Violated tCL + tDout requirement");

  
  
  
  
endmodule
